\begin{tabbing}
ma{-}interface{-}consistent{-}at(${\it es}$;$i$;$X$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=let ${\it ds}$,$F$ = $X$IdDeq($i$)\+
\\[0ex]in
\\[0ex]$\forall$$k$:\{$k$:Knd$\mid$ $\uparrow$hasloc($k$;$i$)\} .
\\[0ex]($\uparrow$fpf{-}dom(KindDeq; $k$; $F$))
\\[0ex]$\Rightarrow$ \=(alle{-}at(${\it es}$;$i$;$e$.(es{-}kind(${\it es}$; $e$) = $k$ $\in$ Knd)\+
\\[0ex]$\Rightarrow$ (es{-}valtype(${\it es}$; $e$) $\subseteq$r ($F$KindDeq($k$).1)))
\\[0ex]\& ($\forall$$x$:Id. es{-}vartype(${\it es}$; $i$; $x$) $\subseteq$r fpf{-}cap(${\it ds}$;IdDeq;$x$;Top)))
\-\-
\end{tabbing}